M:MsgA, a:Id. Dec(a in dom(M.pre)) 

latex

Definitions	MsgA, a in dom(M.pre), Dec(P), x  dom(f), IdDeq, a:A fp B(a), x. t(x), State(ds), Valtype(da;k), locl(a), x:A. B(x), Prop, t  T, Id
Lemmas	Id wf, locl wf, ma-valtype wf, ma-state wf, fpf-trivial-subtype-top, id-deq wf, fpf-dom wf, decidable assert, msga wf